//package useless;
//
//import atom.UnaryAtom;
//import formula.BinaryFormula;
//import formula.UnaryFormula;
//import literal.UnaryLiteral;
//import proof.ConclusionProof;
//import proof.Proof;
//import sign.FormulaSign;
//
//import java.util.ArrayList;
//import java.util.Random;
//
//public class GFV3 {
//    public ArrayList<String> getElement(){
//        String[] alphabet={"a","b","c","d","e","f","g","h","i","j","k","l","m","n",
//                "o","p","q","r","s","t","u","v","w","x","y","z"};
//        ArrayList<String> arr=new ArrayList<>();
//        for (int i = 0; i < 5; i++) {//在alphabet中挑选5个字母作为初始输入
//            Random random=new Random();
//            int randomInt=random.nextInt(26);
//            String atom=alphabet[randomInt];
//            arr.add(atom);
//        }
////        for (String str:arr) {
////            System.out.println(str);
////        }
//        return arr;
//    }
//
//    public UnaryFormula getAtom(ArrayList<UnaryFormula> ufArr1,ArrayList<UnaryFormula> ufArr2){//uf1是atom的list，uf2是not atom的list
//        //70%概率选择atom（false），30%选择not atom（true，即带负号）
//        //返回值是一个被选中的uf
//        Random random = new Random();
//        double randomValue = random.nextDouble();
//        if (randomValue<0.7){//此时从ufArr1中挑选1个atom
//            int index = random.nextInt(5);//同15行选中的初始字母数量
//            return ufArr1.get(index);
//        }else {//此时从ufArr2中挑选1个atom
//            int index = random.nextInt(5);//同15行选中的初始字母数量
//            return ufArr2.get(index);
//        }
//    }
//
//    public BinaryFormula generateBF(ArrayList<String> arr){
//        UnaryFormula uf1=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(0)),false));
//        UnaryFormula uf2=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(1)),false));
//        UnaryFormula uf3=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(2)),false));
//        UnaryFormula uf4=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(3)),false));
//        UnaryFormula uf5=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(4)),false));
//        ArrayList<UnaryFormula> ufArr1=new ArrayList<>();
//        ufArr1.add(uf1);
//        ufArr1.add(uf2);
//        ufArr1.add(uf3);
//        ufArr1.add(uf4);
//        ufArr1.add(uf5);
//
//        UnaryFormula uf6=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(0)),true));
//        UnaryFormula uf7=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(1)),true));
//        UnaryFormula uf8=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(2)),true));
//        UnaryFormula uf9=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(3)),true));
//        UnaryFormula uf10=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(4)),true));
//        ArrayList<UnaryFormula> ufArr2=new ArrayList<>();
//        ufArr2.add(uf6);
//        ufArr2.add(uf7);
//        ufArr2.add(uf8);
//        ufArr2.add(uf9);
//        ufArr2.add(uf10);
//
//        Random randomS=new Random();
//        int sign=randomS.nextInt(2);//random sign
//        if (sign==0){//exist
//            //System.out.println("exist");
//            BinaryFormula bf=new BinaryFormula(FormulaSign.EXIST,getAtom(ufArr1,ufArr2),getAtom(ufArr1,ufArr2));
//            return bf;
//        }else{//any
//            //System.out.println("any");
//            BinaryFormula bf=new BinaryFormula(FormulaSign.ANY,getAtom(ufArr1,ufArr2),getAtom(ufArr1,ufArr2));
//            return bf;
//        }
//    }
//
//    public BinaryFormula generateTF1(ArrayList<String> arr){//tf1 (Exist(a,Exist(b,c)))  c belongs to bf
//        //uf+uf+bf
//        UnaryFormula uf1=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(0)),false));
//        UnaryFormula uf2=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(1)),false));
//        UnaryFormula uf3=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(2)),false));
//        UnaryFormula uf4=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(3)),false));
//        UnaryFormula uf5=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(4)),false));
//        ArrayList<UnaryFormula> ufArr1=new ArrayList<>();
//        ufArr1.add(uf1);
//        ufArr1.add(uf2);
//        ufArr1.add(uf3);
//        ufArr1.add(uf4);
//        ufArr1.add(uf5);
//
//        UnaryFormula uf6=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(0)),true));
//        UnaryFormula uf7=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(1)),true));
//        UnaryFormula uf8=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(2)),true));
//        UnaryFormula uf9=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(3)),true));
//        UnaryFormula uf10=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(4)),true));
//        ArrayList<UnaryFormula> ufArr2=new ArrayList<>();
//        ufArr2.add(uf6);
//        ufArr2.add(uf7);
//        ufArr2.add(uf8);
//        ufArr2.add(uf9);
//        ufArr2.add(uf10);
//
//        Random randomS=new Random();
//        int sign=randomS.nextInt(2);//random sign
//        Random randomS2=new Random();
//        int sign2=randomS2.nextInt(2);//random sign(inner one)
//
//        if (sign==0){//outer sign is exist
//            if (sign2==0){//inner sign is exist
//                //total formula is (E,E)
//                BinaryFormula bfInner=new BinaryFormula(FormulaSign.EXIST,getAtom(ufArr1,ufArr2),generateBF(arr));
//                BinaryFormula bf=new BinaryFormula(FormulaSign.EXIST,getAtom(ufArr1,ufArr2),bfInner);
//                return bf;
//            }else{//inner sign is for any
//                //total formula is (E,A)
//                BinaryFormula bfInner=new BinaryFormula(FormulaSign.ANY,getAtom(ufArr1,ufArr2),generateBF(arr));
//                BinaryFormula bf=new BinaryFormula(FormulaSign.EXIST,getAtom(ufArr1,ufArr2),bfInner);
//                return bf;
//            }
//        }else {//outer sign is for all
//            if (sign2==0){//inner sign is exist
//                //total formula is (A,E)
//                BinaryFormula bfInner=new BinaryFormula(FormulaSign.EXIST,getAtom(ufArr1,ufArr2),generateBF(arr));
//                BinaryFormula bf=new BinaryFormula(FormulaSign.ANY,getAtom(ufArr1,ufArr2),bfInner);
//                return bf;
//            }else{//inner sign is for any
//                //total formula is (A,A)
//                BinaryFormula bfInner=new BinaryFormula(FormulaSign.ANY,getAtom(ufArr1,ufArr2),generateBF(arr));
//                BinaryFormula bf=new BinaryFormula(FormulaSign.ANY,getAtom(ufArr1,ufArr2),bfInner);
//                return bf;
//            }
//        }
//    }
//
//    public BinaryFormula generateTF2(ArrayList<String> arr){//tf2 (Exist(a,Exist(b,c)))  c belongs to uf
//        //uf+uf+uf
//        UnaryFormula uf1=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(0)),false));
//        UnaryFormula uf2=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(1)),false));
//        UnaryFormula uf3=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(2)),false));
//        UnaryFormula uf4=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(3)),false));
//        UnaryFormula uf5=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(4)),false));
//        ArrayList<UnaryFormula> ufArr1=new ArrayList<>();
//        ufArr1.add(uf1);
//        ufArr1.add(uf2);
//        ufArr1.add(uf3);
//        ufArr1.add(uf4);
//        ufArr1.add(uf5);
//
//        UnaryFormula uf6=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(0)),true));
//        UnaryFormula uf7=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(1)),true));
//        UnaryFormula uf8=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(2)),true));
//        UnaryFormula uf9=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(3)),true));
//        UnaryFormula uf10=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(4)),true));
//        ArrayList<UnaryFormula> ufArr2=new ArrayList<>();
//        ufArr2.add(uf6);
//        ufArr2.add(uf7);
//        ufArr2.add(uf8);
//        ufArr2.add(uf9);
//        ufArr2.add(uf10);
//
//        Random randomS=new Random();
//        int sign=randomS.nextInt(2);//random sign
//        Random randomS2=new Random();
//        int sign2=randomS2.nextInt(2);//random sign(inner one)
//
//        if (sign==0){//outer sign is exist
//            if (sign2==0){//inner sign is exist
//                //total formula is (E,E)
//                BinaryFormula bfInner=new BinaryFormula(FormulaSign.EXIST,getAtom(ufArr1,ufArr2),getAtom(ufArr1,ufArr2));
//                BinaryFormula bf=new BinaryFormula(FormulaSign.EXIST,getAtom(ufArr1,ufArr2),bfInner);
//                return bf;
//            }else{//inner sign is for any
//                //total formula is (E,A)
//                BinaryFormula bfInner=new BinaryFormula(FormulaSign.ANY,getAtom(ufArr1,ufArr2),getAtom(ufArr1,ufArr2));
//                BinaryFormula bf=new BinaryFormula(FormulaSign.EXIST,getAtom(ufArr1,ufArr2),bfInner);
//                return bf;
//            }
//        }else {//outer sign is for all
//            if (sign2==0){//inner sign is exist
//                //total formula is (A,E)
//                BinaryFormula bfInner=new BinaryFormula(FormulaSign.EXIST,getAtom(ufArr1,ufArr2),getAtom(ufArr1,ufArr2));
//                BinaryFormula bf=new BinaryFormula(FormulaSign.ANY,getAtom(ufArr1,ufArr2),bfInner);
//                return bf;
//            }else{//inner sign is for any
//                //total formula is (A,A)
//                BinaryFormula bfInner=new BinaryFormula(FormulaSign.ANY,getAtom(ufArr1,ufArr2),getAtom(ufArr1,ufArr2));
//                BinaryFormula bf=new BinaryFormula(FormulaSign.ANY,getAtom(ufArr1,ufArr2),bfInner);
//                return bf;
//            }
//        }
//    }
//
//    public BinaryFormula generateConclusion(ArrayList<String> arr){
//        Random random=new Random();
//        int flag= random.nextInt(3);
//        if (flag==0){//生成bf
//            return generateBF(arr);
//        } else if (flag==1){//生成tf1
//            return generateTF1(arr);
//        }else {//生成tf2
//            return generateTF2(arr);
//        }
//    }
//
//    public Proof run(int numBF,int numTF1,int numTF2){
//        ArrayList<String> element=getElement();
//        System.out.println(element);
//
//        int numConditions=numBF+numTF1+numTF2;
//        int numUf=2*numBF+2*numTF1+3*numTF2;
//        double alpha=(double) (numUf)/(double) numTF1;// uf number/bf number
//        double beta=(double)(numConditions)/(double)(numUf);//formulas(conditions) number/uf number
//
//        ArrayList<Proof> proofs=new ArrayList<>();
//
//        for (int i = 0; i < numBF; i++) {
//            BinaryFormula bf=generateBF(element);
//            System.out.println(bf);
//            proofs.add(new ConclusionProof(bf));
//        }
//        for (int i = 0; i < numTF1; i++) {
//            BinaryFormula bf=generateTF1(element);
//            System.out.println(bf);
//            proofs.add(new ConclusionProof(bf));
//        }
//        for (int i = 0; i < numTF2; i++) {
//            BinaryFormula bf=generateTF2(element);
//            System.out.println(bf);
//            proofs.add(new ConclusionProof(bf));
//        }
//
//        BinaryFormula conclusion=generateConclusion(element);
//        System.out.println(conclusion);
//
//        Proof result= Solve.solveHelper(proofs,conclusion, new UsedCondition());
//        System.out.println(result);
//        System.out.println("alpha = "+alpha);
//        System.out.println("beta = "+beta);
//        return result;
//
//
//    }
//
//    public Integer count(int numBF,int numTF1,int numTF2,int loops){
//        int count=0;
//        for (int i = 0; i < loops; i++) {
//            if (run(numBF,numTF1,numTF2)!=null){
//                count=count+1;
//            }
//        }
//        return count;
//
//    }
//
//    public static void main(String[] args) {
//        GFV3 gf=new GFV3();
//        int count=0;
//        for (int i = 0; i < 5; i++) {
//            Proof proof=gf.run(3,2,2);
//            if (proof!=null){
//                count=count+1;
//            }
//        }
//        System.out.println(count);
//
//        //gf.count(3,2,2,10);
//
//
//
//
//    }
//}
